Previous | 
Home
Section: Software
Software
libalf : the Automata Learning Framework
Participant : Benedikt Bollig [correspondant] .
libalf is a comprehensive, open-source library for learning finite-state automata covering various well-known learning techniques (such as, Angluin s L, Biermann, and RPNI, as well as a novel learning algorithm for NFA. libalf is highly flexible and allows for facilely interchanging learning algorithms and combining domain-specific features in a plug-and-play fashion. Its modular design and its implementation in C++ make it a flexible platform for adding and engineering further, efficient learning algorithms for new target models (e.g., Büchi automata).
Details on libalf can be found at http://libalf.informatik.rwth-aachen.de/
Mole/Cunf: unfolders for Petri Nets
Participants : Stefan Schwoon [correspondant] , César Rodríguez.
Mole computes, given a safe Petri net, a finite prefix of its unfolding. It is designed to be compatible with other tools, such as PEP and the Model-Checking Kit, which are using the resulting unfolding for reachability checking and other analyses. The tool Mole arose out of earlier work on Petri nets. Details on Mole can be found at http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/ .
In the context of MExICo, we have created a new tool called Cunf, which is able to handle contextual nets, i.e. Petri nets with read arcs [42] ,[48] . While in principle every contextual net can be transformed into an equivalent Petri net and then unfolded using Mole, Cunf can take advantage of their special features to do the job faster and produce a smaller unfolding. Cunf has recently been extended with a verification component that takes advantage of these features [70] . More details can be found at http://www.lsv.ens-cachan.fr/~rodrigue/tools/cunf/ . Moreover, Cunf has been integrated into the CosyVerif environment (see section 5.1.4 ).
COSMOS : a Statistical Model Checker for the Hybrid Automata Stochastic Logic
Participants : Hilal Djafri, Benoît Barbot [correspondant] .
COSMOS is a statistical model checker for the Hybrid Automata Stochastic Logic (HASL). HASL employs Linear Hybrid Automata (LHA), a generalization of Deterministic Timed Automata (DTA), to describe accepting execution paths of a Discrete Event Stochastic Process (DESP), a class of stochastic models which includes, but is not limited to, Markov chains. As a result HASL verification turns out to be a unifying framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. COSMOS takes as input a DESP (described in terms of a Generalized Stochastic Petri Net), an LHA and an expression Z representing the quantity to be estimated. It returns a confidence interval estimation of Z; recently, it has been equipped with functionalities for rare event analysis. COSMOS is written in C++ and is freely available to the research community.
Details on COSMOS can be found at http://www.lsv.ens-cachan.fr/ barbot/cosmos/
COSYVERIF
Participants : Serge Haddad [correspondant ?] , Benoît Barbot.
CosyVerif is a software environment whose goal is the formal specification and verification of dynamic systems.
It has been designed in order to:
- support different formalisms with the ability to easily create new ones, - provide a graphical interface for every formalism, - include verification tools called via the interface as a web service, - offer the possibility for a developer to integrate his/her own tool, also allowing it to interact with the other tools.
This environment consists of two software tools: Coloane, the graphical interface, and Alligator, an integration framework based web services. It is enlarged with the existing verification tools developed in our laboratories (founding members or partners). Why ?
The development of Cosyverif has been decided and it is supported by three partners of the Parisian verification group, MeFoSyLoMa. This group is composed of seven teams. and the founding members of are LIP6, LIPN and LSV. First, these members aim at sharing their tools, comparing and supporting industrial case studies and finally making them long-lasting. Second, they also want to promote the practice of formal verification in industry and thus they intend to ease the task of integration of new formalisms and tools.
It is managed by a steering committee consisting of researchers and engineers. It decides strategic orientations as well as technical choices. Current Tools
Two formalisms are supported: automata and Petri nets, both with extensions. Most of the tools are related to Petri nets. Some of them perform structural analyses like invariant computations. while other tools perform behavioural analyses: symbolic reachability graph building, unfolding, stochastic simulations, etc. Finally some of them transform high-level nets into low-level ones. All the developed software are open source and free software tools. Alligator is published under the GNU Affero General Public License (AGPL) version 3 ; Coloane is published under the Eclipse Public License (EPL) version 1 .
Three engineers have worked or are currently working on COSYVERIF: